[e1;e2]~([a,b].p(a;b))*[a,b].q(a;b)
== m:
== f:int_seg(0; m){e:es-E(es)| loc(e) = loc(e1)} 
== (((f(0) = e1)  es-le(es; (f(m - 1)); e2))
==  ((i:int_seg(0; (m - 1)). es-locl(es; (f(i)); (f(i + 1))))
==   (i:int_seg(0; (m - 1)). p(f(i);es-pred(es; (f(i + 1))))))
==  q(f(m - 1);e2)) 

latex

---

clarification:

es-pstar-q(es;a,b.p(a;b);a,b.q(a;b);e1;e2)
== m:
== f:int_seg(0; m){e:es-E(es)| es-loc(es; e) = es-loc(es; e1)  Id} 
== (((f(0) = e1  es-E(es))  es-le(es; (f(m - 1)); e2))
==  ((i:int_seg(0; (m - 1)). es-locl(es; (f(i)); (f(i + 1))))
==   (i:int_seg(0; (m - 1)). p(f(i);es-pred(es; (f(i + 1))))))
==  q(f(m - 1);e2)) 

latex

Definitions	[e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), , x:A. B(x), Id, loc(e), es-E(es), es-le(es; e; e'), P  Q, es-locl(es; e; e'), x:A. B(x), int_seg(i; j), es-pred(es; e)
FDL editor aliases	es-pstar-q